p, q:(n:base-domain-type(n)). p = q   

latex

Definitions

t  T, x:A. B(x), a = b, P & Q, Knd, IdLnk, x.A(x), x. t(x), 2of(t), a = b, 1of(t), p  q, Id, a = b, base-domain-type(n), {T}, P  Q, SQType(T), , s = t, Prop, s ~ t, False, A, left+right, P  Q, true, x:AB(x), #$n, b, b, x:AB(x), Type, True, , p  q, T, P  Q, P  Q, Unit, false, if b t else f fi, p = q, i=j

Lemmas

base-domain-type wf, ifthenelse wf, bfalse wf, eqtt to assert, assert of bor, or functionality wrt iff, eqff to assert, squash wf, true wf, bnot thru bor, assert of band, and functionality wrt iff, iff transitivity, assert of bnot, not functionality wrt iff, assert of eq int, bor wf, bool wf, bnot wf, not wf, assert wf, eq int wf, btrue wf, eq id wf, Id wf, band wf, pi1 wf, eq lnk wf, pi2 wf, IdLnk wf, Knd wf, eq knd wf